COMMENT ⊗   VALID 00003 PAGES 
RECORD PAGE   DESCRIPTION
 00001 00001
 00002 00002	
 00003 00003	
 00004 ENDMK
⊗;


STANFORD ARTIFICIAL INTELLIGENCE PROJECT              SEPTEMBER 1973
OPERATING NOTE 73







.BEGIN CENTER





PRELIMINARY USER'S MANUAL
FOR
AN
INTERACTIVE THEOREM PROVER

BY

JOHN ALLEN
.END










ABSTRACT:


.BEGIN DOUBLE SPACE
This document represents a short guide to using the theorem prover.  An earlier
version of this program is described in Allen and Luckham [MI5].  
Many of the later sections of this manual,
on pattern matching and subroutining especially, are still in a rudimentary
stage of development. Experiments demonstrating various applications of the strategies
and the user oriented features are described in a forthcoming report,
"Applications of First Order Proof Procedures" by Allen, Luckham, and Morales.
.END